数学における証明と真理 第2部メモ
なおここでの議論は別に帰納法を使っているわけではなさそうなので，Robinson算術$ \mathsf{Q}でも成り立つ気がする．
$ Tを理論とする．
$ \text{Prf}_T(x,y)は「$ yは，$ xをGödel数として持つ論理式$ E_xの$ Tでの証明のGödel数」を表す$ \Delta_1論理式とする．
$ \text{Pr}_T( x ):= \exists_y. \text{Prf}_T ( x,y )は，$ Tの証明可能性述語と呼ばれる． 「$ E_xは証明可能である」を意味する．
$ \Sigma_1論理式．
$ Tを理論とする．
任意の文$ \varphi,\psiについて，$ \mathsf{PA} \vdash \text{Pr}_T \left( \overline{\ulcorner \varphi \urcorner} \right) \leftrightarrow \text{Pr}_{T+\varphi} \left( \overline{\ulcorner \psi \urcorner} \right)
再帰的可算な理論$ T，任意の論理式$ \varphi,\psiについて次が成り立つ．
D1. $ T \vdash \varphi$ \implies$ \mathsf{PA} \vdash \mathrm{Pr}_T \left(\overline{\ulcorner \varphi \urcorner}\right)
D2. $ \mathsf{PA} \vdash \mathrm{Pr}_T \left( \overline{\ulcorner \varphi \to \psi \urcorner} \right) \to \left( \mathrm{Pr}_T \left( \overline{\ulcorner \varphi \urcorner} \right) \to \mathrm{Pr}_T \left( \overline{\ulcorner \psi \urcorner} \right) \right)
D3. $ \mathsf{PA} \vdash \text{Pr}_T\left( \overline{\ulcorner \varphi \urcorner}\right) \to \text{Pr}_T\left(\overline{\ulcorner\mathrm{Pr}_T\left(\overline{\ulcorner\varphi\urcorner}\right)\urcorner}\right)
定理: 形式化された$ \Sigma_1完全性
$ Tを理論とする．
任意の$ \Sigma_1文$ \varphiについて，$ \mathsf{PA} \vdash \varphi \to \mathrm{Pr}_T\left(\overline{\ulcorner \varphi \urcorner}\right)
特に，$ \varphi = \mathrm{Pr}_T\left(\overline{\ulcorner \psi \urcorner}\right)とすると導出可能性条件の3が得られる． 定義: $ \mathrm{Con}_T
$ Tを理論とする．
$ \botは例えば$ \mathbf{0} = s(\mathbf{0})のような反証可能な$ \Sigma_1文が入るとする
$ \mathrm{Con}_T = \lnot\mathrm{Pr}_T(\overline{\ulcorner\bot\urcorner})は$ Tの無矛盾性を表す述語．
$ \Pi_1文．
$ \lnot \mathrm{Pr}_T(\overline{\ulcorner \bot \urcorner}) = \lnot\exists_ y.\mathrm{Prf}_T(\bot,y) = \forall_y.\lnot\mathrm{Prf}_T(\bot,y)
自由変数を$ xのみ持つ論理式$ \varphi(x)に対し，次の文$ \psiが存在する．
$ \mathsf{PA} \vdash \psi \leftrightarrow \varphi\left( \overline{\ulcorner\psi\urcorner} \right)
特に，$ \varphi(x)が$ \Sigma_n論理式なら$ \psiも$ \Sigma_n文，$ \varphi(x)が$ \Pi_n論理式なら$ \psiも$ \Pi_n文．
系1
$ Tを$ \mathsf{PA}の再帰的可算な拡大理論とする．
$ \lnot \mathrm{Pr}_T(x)は$ \Pi_1論理式であるので，不動点補題を適応すると，次の$ \Pi_1文$ \piが存在する． $ \mathsf{PA} \vdash \pi \leftrightarrow \lnot\mathrm{Pr}_T\left(\overline{\ulcorner\pi\urcorner} \right)
ここから，
$ T \vdash \pi \leftrightarrow \lnot\mathrm{Pr}_T\left( \overline{\ulcorner\pi\urcorner} \right)
$ Tを$ \mathsf{PA}の再帰的可算な拡大理論とする．$ \piを$ TのGödel文とする． 1. $ Tが無矛盾なら，$ T \not\vdash \pi
2. $ Tが$ \Sigma_1健全なら，$ T \not\vdash \lnot\pi
補題1: $ \Sigma_1健全と無矛盾性
理論$ Tが$ \Sigma_1健全なら，無矛盾．
$ Tを$ \mathsf{PA}の再帰的可算かつ$ \Sigma_1健全な拡大理論とし，$ \piを$ TのGödel文とする．
$ T \not \vdash \piかつ$ T \not \vdash \lnot\pi
補題2
任意の$ \mathsf{PA}の再帰的拡大理論$ T，任意の文$ \varphiに対し
$ \mathsf{PA} \vdash \lnot\mathrm{Pr}_T\left(\overline{\ulcorner \varphi \urcorner}\right) \to \mathrm{Con}_T
補題3
任意の$ \mathsf{PA}の拡大理論$ T,U，任意の文$ \varphiに対し，1と2は同値．
1. $ U \vdash \mathrm{Con}_T \to \lnot \mathrm{Pr}_T\left( \overline{\ulcorner \varphi \urcorner} \right)
2. $ U \vdash \mathrm{Pr}_T\left( \ulcorner \varphi \urcorner \right) \to \mathrm{Pr}_T \left( \ulcorner \lnot\varphi \urcorner \right)
補題4
$ TのGödel文$ \piに対し
$ T \vdash \mathrm{Con}_T \to \lnot\mathsf{Pr}_T \left(\overline{\ulcorner \pi \urcorner}\right)
証明
1. $ \mathsf{PA} \vdash \lnot\pi\to \mathrm{Pr}_T\left(\overline{\ulcorner \lnot\pi \urcorner}\right)
形式化された$ \Sigma_1健全性
2. $ T \vdash \lnot\pi\to \mathrm{Pr}_T\left(\overline{\ulcorner \lnot\pi \urcorner}\right)
1の拡大
3. $ T \vdash \lnot\pi \leftrightarrow \mathrm{Pr}_T\left( \overline{\ulcorner\pi\urcorner} \right)
$ \piの定義より．
4. $ T \vdash \mathrm{Pr}_T\left( \overline{\ulcorner\pi\urcorner} \right) \to \mathrm{Pr}_T\left( \overline{\ulcorner\lnot\pi\urcorner} \right)
2,3
5. $ T \vdash \mathrm{Con}_T \to \lnot \mathrm{Pr}_T\left( \overline{\ulcorner \pi \urcorner} \right)
4, 補題3の2→1
$ TのGödel文$ \piについて
$ T \vdash \pi \leftrightarrow \mathrm{Con}_T
証明
1. $ T \vdash \lnot\mathrm{Pr}_T\left(\overline{\ulcorner \pi \urcorner}\right) \to \mathrm{Con}_T
補題2の$ \varphiとして$ \piとし，拡大．
2. $ T \vdash \lnot\mathsf{Pr}_T(\overline{\ulcorner \pi \urcorner}) \leftrightarrow \mathrm{Con}_T
1と補題4
3. $ T \vdash \pi \leftrightarrow \lnot\mathrm{Pr}_T\left( \overline{\ulcorner\pi\urcorner} \right)
$ \piの定義，対偶．
4. $ T \vdash \pi \leftrightarrow \mathrm{Con}_T
1,2
系2
$ Tの任意のGödel文$ \pi,\pi'について
$ T \vdash \pi \leftrightarrow \pi'
$ Tを$ \mathsf{PA}の再帰的可算な拡大理論とする．
1. $ Tが無矛盾なら$ T \not\vdash \mathrm{Con}_T
2. $ Tが$ \Sigma_1健全なら$ T \not\vdash \lnot \mathrm{Con}_T
命題
$ \mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA} \vdash \lnot \mathrm{Con}_{\mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA}}
証明
1. $ \mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA} \vdash \lnot\mathrm{Con}_\mathsf{PA}
2. $ \mathsf{PA} \vdash \lnot\mathrm{Pr}_\mathsf{PA}(\overline{\ulcorner \mathrm{Con}_\mathsf{PA} \urcorner}) \to \mathrm{Con}_\mathsf{PA}
補題4.2.3: $ Tとして$ \mathsf{PA}，$ \varphiとして$ \mathrm{Con}_\mathsf{PA}
3. $ \mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA} \vdash \lnot\mathrm{Pr}_\mathsf{PA}(\overline{\ulcorner \mathrm{Con}_\mathsf{PA} \urcorner}) \to \mathrm{Con}_\mathsf{PA}
2の拡大．
4. $ \mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA} \vdash \lnot\mathrm{Con}_\mathsf{PA} \to \mathrm{Pr}_\mathsf{PA}(\overline{\ulcorner \mathrm{Con}_\mathsf{PA} \urcorner})
3の対偶
5. $ \mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA} \vdash \mathrm{Pr}_\mathsf{PA}(\overline{\ulcorner \mathrm{Con}_\mathsf{PA} \urcorner})
1,4
6. $ \mathsf{PA} \vdash \mathrm{Con}_\mathsf{PA} \leftrightarrow \lnot\lnot \mathrm{Con}_\mathsf{PA}
7. $ \mathsf{PA} \vdash \mathrm{Con}_\mathsf{PA} \leftrightarrow (\lnot \mathrm{Con}_\mathsf{PA} \to \bot )
8. $ \mathsf{PA} \vdash \mathrm{Pr}_\mathsf{PA} \left(\overline{\ulcorner \mathrm{Con}_\mathsf{PA} \urcorner}\right) \leftrightarrow \mathrm{Pr}_\mathsf{PA}\left(\overline{\ulcorner \lnot \mathrm{Con}_\mathsf{PA} \to \bot \urcorner} \right)
7, 導出可能性条件D1
9. $ \mathsf{PA} + \lnot\mathrm{Con}_\mathsf{PA} \vdash \mathrm{Pr}_\mathsf{PA} \left(\overline{\ulcorner \mathrm{Con}_\mathsf{PA} \urcorner}\right) \leftrightarrow \mathrm{Pr}_\mathsf{PA}\left(\overline{\ulcorner \lnot \mathrm{Con}_\mathsf{PA} \to \bot \urcorner} \right)
8の拡大
10. $ \mathsf{PA} + \lnot\mathrm{Con}_\mathsf{PA} \vdash \mathrm{Pr}_\mathsf{PA}\left(\overline{\ulcorner \lnot \mathrm{Con}_\mathsf{PA} \to \bot \urcorner} \right)
5,9
11. $ \mathsf{PA} + \lnot\mathrm{Con}_\mathsf{PA} \vdash \mathrm{Pr}_\mathsf{PA}\left(\overline{\ulcorner \lnot \mathrm{Con}_\mathsf{PA} \urcorner} \right) \to \mathrm{Pr}_\mathsf{PA}\left(\overline{\ulcorner \bot \urcorner} \right)
10, D2
12. $ \mathsf{PA} + \lnot\mathrm{Con}_\mathsf{PA} \vdash \mathrm{Pr}_{\mathsf{PA} + \lnot \mathrm{Con}_\mathsf{PA}}\left(\overline{\ulcorner \bot \urcorner} \right)
13. $ \mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA} \vdash \lnot \mathrm{Con}_{\mathsf{PA}+\lnot\mathrm{Con}_\mathsf{PA}}
12, $ \mathrm{Con}_Tの定義より
任意の文$ \varphiに対し，1と2は同値．
1. $ T \vdash \varphi
2. $ T \vdash \mathrm{Pr}_T(\overline{\ulcorner \varphi \urcorner}) \to \varphi
証明: 1→2
自明．
2を仮定する．
対偶と演繹定理より$ T + \lnot \varphi \vdash \lnot \mathrm{Pr}_T(\ulcorner \varphi \urcorner)
導出可能性条件D2の対偶$ T \vdash ( \mathrm{Pr}_T ( \overline{\ulcorner \varphi \urcorner} ) \land \lnot \mathrm{Pr}_T ( \overline{\ulcorner \psi \urcorner} ) ) \to \lnot \mathrm{Pr}_T ( \overline{\ulcorner \varphi \to \psi \urcorner} )
より，$ T + \lnot\varphi \vdash ( \mathrm{Pr}_T ( \overline{\ulcorner \lnot \varphi \urcorner} ) \land \lnot \mathrm{Pr}_T ( \overline{\ulcorner \bot \urcorner} ) ) \to \lnot \mathrm{Pr}_T ( \overline{\ulcorner \lnot \varphi \to \bot \urcorner} )
更に，$ T + \lnot\varphi \vdash ( \mathrm{Pr}_T ( \overline{\ulcorner \lnot \varphi \urcorner} ) \land \mathrm{Con}_T ) \to \lnot \mathrm{Pr}_T ( \overline{\ulcorner \lnot \varphi \to \bot \urcorner} )
Lem2より$ T + \lnot\varphi \vdash \mathrm{Con}_T
よって$ T + \lnot \varphi \vdash \lnot \mathrm{Pr}_T ( \overline{\ulcorner \lnot \varphi \to \bot \urcorner} )
形式化された演繹定理より$ T + \lnot \varphi \vdash \lnot \mathrm{Pr}_{T + \lnot \varphi} (\overline{\ulcorner \bot \urcorner} )
第2不完全性定理より$ T + \lnot\varphiは矛盾する．
$ \varphiは↓を満たすとき，$ \varphiはHenkin文という． $ T \vdash \varphi \leftrightarrow \mathrm{Pr}_T\left( \overline {\ulcorner\varphi\urcorner} \right)
1. $ Tは無矛盾とする．
2. $ T \vdash \mathrm{Con}_Tと仮定する．
3. $ T \vdash \lnot \mathrm{Pr}_T\left( \overline{\ulcorner\bot\urcorner}\right)
$ \mathrm{Con}_Tの定義
4. $ T \vdash \mathrm{Pr}_T\left( \overline{\ulcorner\bot\urcorner}\right) \to \bot
$ \lnotの定義
5. $ T \vdash \bot
6. $ T \not\vdash \bot
$ Tの無矛盾性より．
6. 破綻．仮定2は誤り．$ T \not\vdash \mathrm{Con}_T